es:ES, e:E. state after e  state@loc(e) 

latex

Definitions

t  T, x:A. B(x), P  Q, loc(e), f(a), Id, x:AB(x), x.A(x), x. t(x), 2of(t), es-pred!(es;e;e'), SWellFounded(R(x;y)), <a,b>, s = t, pred!(e;e'), first(e), b, A, loc(e), IdLnk, kind(e), Type, x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), S  T, S  T, state@i, vartype(i;x), Knd, when-after(e;info;pred?;init;Trans;val), state after e, ES, es_val(es), es-Trans(es), es_init(es), es_info(es), es-pred?(es), es-M(es), es-V(es), es-T(es), E

Lemmas

event system wf, when-after wf, es info wf, es init wf, es-Trans wf, Knd wf, es-state wf, es val wf, kindcase wf, es-kind wf, es-V wf, es-M wf, IdLnk wf, not wf, assert wf, first wf, es-pred? wf, es-E wf, pi2 wf, Id wf, es-T wf, es-loc wf, es-loc-pred, es-pred!-wellfounded